WIP: improve certified kernel and certify compilation - #665

A read the collapse drops whole has an empty segment and reads to
nothing, so the trace's segments now handle it directly and need the
level-parameter and self-reference facts only for kept reads. Those come
from quotient Source's acceptance: every declaration the trace keeps is
in the accepted prepared stream.

TraceNeeds gains levels (distinct level positions of every kept
declaration) in place of the per-group nodup and levels premises of
definitions and definition blocks; HeaderNeeds takes nodup and noSelf
under the kept read. New module TraceSource: kept_mem, kept_levels,
accepted_axiom (an accepted axiom's level positions are distinct, or it
is the pinned quotient soundness record and has one level parameter) and
axiom_nodup. readerStreams_of_units passes the trace's prepared-stream
equations to its units premise.

BoundResolve, the fold premise of the segment readings' compile-side
contexts, asks that every address a block's snapshot binds holds a
stored record that resolves. It holds for every state of the fold's run
(boundResolve_onRun), given that every input inductive's j-th
constructor declares index j (ConstructorIndices, the meaning of the
compile report's constructor index check): the compiler stores the
declared index and addresses the constructor by its position.

Every reached state's bindings resolve in its own store (reach_boundOK):
a step keeps the old bindings in a larger store, and a new binding is a
claim of a checked merge, which stores its block record, and resolves
by runBlock_claims. A run state's records persist into the artifact.

claimedIn_bound: claimedIn_of with BoundResolve at the claim's snapshot.

The inductive group readings asked every family recursor's index entry
for a major premise in the group's own block, with the block's
constructors for its rules. A nested family's auxiliary recursor
eliminates its container instead: Lean's Tree.rec_1 for a Tree with a
List Tree field has a major premise of type List Tree, which the index
records as the container's member, and its rules are List's
constructors. So every closure with a nested inductive failed the
premise.

entries in compiled_inductive_unit_reads, closure_inductive_reads and
InductiveCompiled now take any major member .member mb mi, an inductive
of the reading store with a constructor per rule, the rules'
constructors keyed at mb, as InductiveUnits.RecFacts already does. The
inductive block's store premise of compiled_inductive_unit_reads was
used only for the in-block major and is dropped.

Quotient Source groups an inductive family by its first type's Lean block,
while the compiler compiles the strongly connected components of the input's
reference graph. On crafted input the two can differ: a recursor's own all
field joins it to another family's recursors in the reference graph, and
Source reads only all[0]. The compile report is to check that every component
holding a family member is one family's; its meaning, FamilyBlocks, is a
named premise here until the check lands.

New module Ix/Cert/FamilyGroups.lean:
- inductiveGroup_shape: an inductive block's group is refused or has its
  block's shape (TypesOf, CtorsOf, blockRecursors), read off its loops
  (forIn_collect).
- groups_origin: a group of groupsOf is an inductive block's, with the
  recursors tabled under its first member (recsTable), a component's, or an
  unplaced constant's.
- inductive_block: under FamilyBlocks, the compile block of a Source
  inductive group's first type holds exactly the group's types and
  constructors.
- recursor_block: under FamilyBlocks, the compile block of one of its
  recursors holds exactly the group's recursors. Every input recursor of the
  block is in the closure, in a group that converts, and that group is this
  one.

The compile report now checks that literal-support roles are named
(ReportChecks: LiteralRolesNamed, literalRoleName). LayoutExtra drops its
local copies of both, and layout_extra_of takes the check from the report
(literalRolesNamed) in place of a premise.

assembleEnv now inserts the store's blobs last, over the name-component
blobs, so the artifact holds each stored blob with its bytes
(assembleEnv_blob, from StepKeeps.fold_insert_last). The blob conjuncts of
compileEnvFold_provenanceFresh, compileReport_owned_block_of and
compileReport_owned_blobs now give the artifact's bytes, not only that a
blob is there.

The checker installs a quotient record only when it matches its pin up to
the canonical renumbering of level parameters. The pins of one parameter
force one name. Quot.lift's pin has two, and its canonical type mentions
the second position; a term numbered under two equal names mentions only
position 0 and the past-the-end position, and the canonical forms keep
that set. So the record's two names are distinct.

TraceSource gains the level-position lemmas (ingress, key renaming,
mapLevels, canonLevelIn through canonUniv_occurs, canonExpr),
pinned_quot_nodup and quotient_nodup, which discharges HeaderNeeds.nodup
for quotient constants.

The literal-role check refused every artifact that stores a record at a
literal-support role's address (the `Nat` basis, the string support)
without that role's name published there. That refuses any closure
holding an α-copy of `Nat`, `List`, `String` or `Char` without the
original, which is common in user code: `inductive MyNat | zero | succ`
compiled as a selected closure lands at `Nat`'s address.

A role matters only when a literal is checked against it, so the check
now constrains a literal kind's support roles only when some stored
record holds a literal of that kind (`Ix.Kernel.Reader.literalKinds`:
the `Nat` basis for a `Nat` literal, with the string support for a
`String` literal). `LiteralRolesNamed env ixe` is restated per stored
record: for `recordAt ixe a = some c` and `s ∈ literalRoles c`, a stored
record at `s`'s bound address is `s`'s name, published there. The
decider first finds the bound literal-support roles stored without
their name, as before; only when there is one does it read the stored
records' literal kinds (`storedLiteralKinds`, on tasks), so real inputs
never walk the records. Compiled output is unchanged.

Audit (`Ix/Cert/Audit.lean`): `checkReport` re-frozen because its
literal-role message now says the role is one a stored literal is
checked against; the literal-role section re-frozen for the restated
`LiteralRolesNamed` and its new lemmas and runtime definitions (8 roots,
7 safe definitions; standard axioms, no runtime substitution).

Tests: in `cert-statement`, `AdvNat` (an α-copy of `Nat`) compiled
without `Nat` is now accepted alone, and still refused by the
literal-role check beside a crafted `Nat` literal at type `AdvNat`.
`compile-ind-flags`' recursive fixture `T` is back to
`leaf | node : T → T`, which the narrowed check accepts.

The checker's shape guard on an inductive declaration (checkDecl_noCtor)
refuses a block one of whose constructor keys occurs in a former's or a
constructor's type, for any number of types. A kept inductive group
lowers to such a declaration over its members' types renamed to
representatives with canonical levels, so a constructor's Lean name in a
source type would give its renamed key in the declared one.

inductive_noCtor discharges InductiveNeeds.noCtor from the trace's
lowering and the acceptance of the prepared stream, through
convertInductive_entries, lowerInductive_decl and noCtorIn_of_ingress;
mentionsConst_substKeys carries a key through the renaming.

The compile lays a recursor block out by recursorFamilyPosition, which
reads each recursor's own all field, while quotient Source orders an
inductive group's recursors by its first type's all and reads only
all[0] of a recursor's. A crafted recursor all that permutes the family
reorders the compiled block against Source's. The family-blocks check's
recursor clause now also requires every recursor of a recursor block to
carry its family's first inductive's all, and the family to have fewer
than 2^63 members and auxiliaries, as positions are 64-bit.

Ix.CompileCert.Canon.QSort shows that Array.qsort permutes its input. The
new module QSortSorted shows that it sorts: for an irreflexive, transitive
comparison, no element of the output is less than one before it
(qsort_pairwise), through the private sort and qpartition.loop. The
partition rearranges its segment within itself and puts the elements less
than the pivot before it and the others after it; the median of three
keeps an element that is not less than the pivot below the segment's end,
so the pivot never lands at the end. Two qsorts of permutations of each
other are then equal when the comparison orders any two distinct elements
(qsort_eq_of_perm).

A lowered inductive group of quotient Source's graph is inductiveGroup's
for a block of the closure (FamilyGroups.inductive_origin), which either
refuses the block or reads the types' constructor lists off it, each
constructor declaring its position (FamilyGroups.inductiveGroup_shape).
inductive_shape gives InductiveNeeds.hcsize and positions from that.

Bring in the family-blocks premise's requirement that a recursor carry
its family's all, with a size bound, and a general proof that
Array.qsort sorts under a strict order. Proofs only; disjoint from the
reader and links proofs merged since.

The reader's recursor index scanned the stream's records and then the
prelude fallback's. A fallback recursor whose carriers resolve, through
the stream's store, into a block the stream supplies was filed under
that block at any motive the stream's own recursors left free. A stream
copying an Init family byte for byte, without one of its recursors,
then read its block with the prelude's recursor, a record it does not
hold.

contextOf now builds the index over indexedRecords: the stream's
records, then the fallback's it does not shadow, less the fallback
records with a recursor member analysed into a block the stream
supplies (fallbackIndexed). The keys are computed over the same records
as before. A block the stream supplies brings its own recursors: such a
block without one now declines, as every other block without its
recursor already did. Streams that supply their families' recursors
read as before.

contextWith takes the index's records as a parameter, by default its
records. ReaderClosureKeys.selected_origin reads the index's origin
through the sub-array (mem_indexed_scanned); its statement is unchanged.
SourceContext.stream_agrees proves its blob and hint fields by
unfolding the two contexts: rfl between them had the kernel compare the
contexts whole, which now times out on the index's records.

The runtime-closure audits whose entries reach contextOf are refrozen,
each by four compiled functions:
- IxC/Kernel/Audit/Roots.lean: readRecords and readStream 2211 to 2215,
  the checking entries 5985 to 5989, the tiered entries 6095 to 6099;
- IxC/Kernel/Admission/Audit.lean: 5982 to 5986;
- Ix/Ixon/Projection/Audit.lean: 6007 to 6011;
- Ix/Ixon/BlockOrder/Audit.lean: 6145 to 6149;
- Ix/Ixon/Authenticated/Audit.lean: 6164 to 6168, tiered 6105 to 6109;
- Ix/RoleBinding/ArtifactAudit.lean: check and checkAt 6021 to 6025,
  checkTiered and checkTieredAt 6155 to 6159;
- Ix/HostAdmission/Audit.lean: 6414 to 6418.
The four are fallbackIndexed, indexedRecords and their compiled
auxiliaries, reached through contextOf; externs, implemented_by, unsafe,
csimp and the ruling counts are unchanged.

The reader tests copy Nat's family from the prelude: with its recursor
the stream reads; without it the prelude's recursor, which the analysis
files under the copied block, is left out of the index and the block
declines.

A lowered inductive group's first type and each of its recursors have
distinct level-parameter names when quotient Source accepts its prepared
stream. The checker installs the group's indDecl either as a pinned
block or through its modeled or native route:

- not pinned: the modeled route checks every member's level positions
  distinct (ConstantValRun in the member fold and the recursor
  provisioning), the native route its one former's and one recursor's
  (checkConstantVal);
- pinned: every member matches a pin's member canonically, so it has at
  most two names, and a pin's member with two (Eq.rec, PUnit.rec) has a
  canonical type that mentions the second position, which a term
  numbered under two equal names cannot (own or large numbering).

NoCtor.lowerInductive_decl now names the block's recursors
(recInfosOf) instead of hiding them; its two users generalize them as
before. canonLevel_defined and canonExpr_defined map one list of
positions into another. recLevels_of assembles InductiveNeeds.recLevels
from the distinctness and the family's shared list.

A lowered inductive group's types and constructors have its first
type's level-parameter names, and its recursors one list, under the
family check FamilyLevelParams (defined here until the compile report's
checks carry it): the group's types are the inductives its head lists,
its constructors theirs, and its recursors those of its head's family,
all stored in the input environment. Quotient Source numbers each
constant by its own list, so these facts cannot come from its
acceptance.

IxC's checker looks up every constant of a term it accepts. Inference
looks up each constant node and infers every subterm, an application's
argument included, and refuses a let. Annotation keeps every constant
node except a let's type and value, whose annotations it infers before
taking the reduct. A new module, CheckedConsts, proves both facts over
the constant nodes of a term (ConstsAll), so whatever holds of the
constants the checker finds and of the annotated term's constants
holds of the input's. With the ingress's node-for-node correspondence
between a Lean term's constants and its conversion's keys, these facts
can be reused for other properties of accepted source terms.

An axiom's front door runs in an environment without the axiom, so a
kept axiom's type does not name it. The pinned quotient soundness
record and the quotient constants match pins whose types do not name
them, checked by decide.

The compiler lays a block out with sourceClasses: its members sorted by
Ix.sourceOrderLt on their positions and names, ties broken by input
order. Quotient Source orders a group of definitions by the same
comparison. New module Ix/Cert/LeanOrder.lean:

- Name.leanCmp is oriented (leanCmp_swap) and transitive
  (leanCmp_chains), and names it ties have one ingress name
  (ingressName_of_eq);
- so sourceOrderLt is a strict weak order (lt_irrefl, lt_trans,
  lt_of_lt_of_le, lt_of_le_of_lt, le_trans), and keys neither of which is
  before the other tie (tie_of_not_lt);
- sourceClasses_eq: sourceClasses cs = xs.map ([.]) for any permutation
  xs of cs that is sorted and in which no two members tie, from
  Canon.qsort_pairwise and List.Perm.eq_of_pairwise.

The reader's segment theorems take each quotient Source group's compile
run in the group's own order. New module Ix/Cert/GroupRuns.lean:

- runBlock_paths: a block runs alone when it is one non-inductive
  constant, and otherwise runs its members' loop from the empty state
  and compileMutualBlock (sourceClasses cs); membersLoop_eq reads the
  loop as one member per name (memberOf).
- FoldBlock packages the fold's facts about a closure name's block:
  the run and the state it ran at, the publication, freshness, the
  resolution at that state and exact blobs (foldBlock_of).
- definitions_run: a definitions group of two or more runs
  compileMutualBlock over defsOf members. No two members tie: names
  with one ingress key have one published address (addr_of_key, from
  the premises alone), and BlockPublication.apart keeps a block's
  members apart.
- types_run: an inductive group's types run over indsOf types ctors,
  each at its position in its block, given distinct member keys.
- recursors_run: the recursors run as a family in blockRecursors'
  order, or alone under their own name. Each sits at its declared
  position: X.rec at X's, first.rec_j after the block, with the
  decimal digits read back (position_own, position_aux) and the
  family check's 2^63 bound keeping positions exact.
- definitions_compiled, types_compiled and recursors_family state
  these as the run fields of TraceSegments.BlockCompiled and
  InductiveCompiled.

FamilyGroups gains inductive_block_at and recursor_block_at, for any
block holding one of the group's types, resp. recursors;
inductive_block and recursor_block now use them.

Use a local depth budget for the whole-block collapse theorem and the representative-scope conversions throughout the TraceGood proof module. The expanded role-key lookup exceeds the old elaboration default; theorem statements and all axiom guards remain unchanged.

Use a scoped recursion budget for the unchanged inductive-name distinctness argument over the expanded role-key lookup. The reader-stream and closing compiler theorem statements and their axiom guards remain unchanged.

Populate every parent name in the generated-artifact fixture so its bytes
satisfy the canonical name-order gate. Preserve whole-row rejection when a
proof cannot resolve, and check that string support is removed only with
its dependent operations. Match the current no-equations refusal text.

Regenerate the role-table wire corpus from the IxC producer: 44 added
single-role cases and one expanded all-roles case; the other 63 cases are
unchanged. Strict reader checks and producer roundtrips pass for 108 cases.
The production reader and its rejection guards are unchanged.

Require a nonempty contiguous well-founded block before the first equation
group. Preserve the original validation context within that block; later
equation groups may use its operations only through lazy admission. Own and
later equation fast paths remain unavailable.

Carry the reviewed producer output verbatim. The generator rejects two
reorderings that satisfy the prior coverage and dependency conditions.
Isolated original and candidate controls, malformed evidence checks, and
complete binding validation passed. Generated backend and integrated gates
remain required for this combined source.

Require and traverse all 103 roles in a complete binding. The literal class
still consists of the same twelve implicit roles at their existing indices.
The previous 59-entry requirement rejected complete expanded bindings.
Circuit and trace outputs must be regenerated from this source.

A catalog member without a complete binding cannot be promoted to a literal
class. Retain its original validated claim and use catalog joins, while
complete bindings still share class folds. Exercise mixed and partial-only
plans and the actual catalog circuit; retain cross-binding rejection of
incomplete tables.

Prepare Lean 4.29 exports without String.back or its two certificates,
requiring every other role. Preserve the literal-support comparison and
check that this partial table cannot acquire a class. The regenerated
4.29 fixture and integrated gates follow separately.

Run the pinned exporter against strictly elaborated expanded certificates,
omitting only String.back and its two certificate roots. Preserve the
previous fixture in the producer receipt. The compressed export is copied
verbatim from the producer and checked against its SHA256; consumer and
four-toolchain aggregation checks remain required.

Copy the producer outputs for the validated Nat frontier and complete
103-role aggregation table. Regenerate Rust execution, trace, and CUDA
outputs from the strictly checked source; verify every copied SHA256.
Both producer checks pass. No generated file was merged by hand, and the
single final FFT repin remains pending.

Replace stale claims of in-block alpha collapse, auxiliary regeneration, and call-site rewriting with the source layouts that the current fixture corpus exercises. Keep declarations, names, executable tests, and assertions unchanged. Clarify that the corpus compares identical inputs across implementations and schedules, without asserting permutation invariance.

Validation: strict standalone source terminology check passed all 1,964 files; reviewed the comment-only diff and checked that its reverse applies. No new tests or dependency builds were needed.

The Rust backend bypasses compileReport but still passes through role finalization and checkFinalized before publication. State that boundary in --rust help without implying CompileCorrect coverage or an unmeasured performance guarantee.

Validation: traced runCompileCmd through publish and RoleBinding.Compile.finalize/checkFinalized. The strict standalone source terminology check passed all 1,964 files, and the reverse patch check passed. This changes only a help string; no dependency build or remote run was started during the coordinated hold.

Integrate the reviewed fixture narration and Rust-help corrections.
Keep the frozen native baseline as an ancestor; no executable behavior or
test assertions change. Native link caches remain at the measured baseline.

Validate Char.ofNat as a dependency when String.back synthesizes its result,
including claims that assume their binding. Retain ordinary and assumed
consumer controls and the earlier well-founded evidence checks.

Strict source/link and fresh interpreter controls pass. Generated backends
and exact native parity must be refreshed and gated before publication.

Name the raw streamed and Rust entry points used by the closure, schedule, and publication fixtures, and separate their checks from CLI finalization. Replace obsolete collapse/rewriting history and private queue references with the current source-order, reconstruction, and closure assertions. Preserve every declaration, identifier, log label, and executable assertion.

Validation: inspect the actual harness, schedule, FFI, and closure callers; the strict standalone source terminology check passed all 1,965 files, and the reverse patch check passed. The extra scanned file is the already integrated BindingFrontier module. All changes are comments; no dependency build or remote work was run during performance calibration.

Describe --rust-check as a raw Rust handoff followed by shared finalization and Lean serialization on both final envelopes. State that a later mismatch leaves the Lean output already written. Explain that fail-closed compilation failures leave an absent or existing destination untouched and that --allow-partial permits the successfully compiled subset.

Validation: traced both compile commands through their failure checks, finalization, serialization, and atomic writes; inspected the retained existing/absent destination controls. The strict standalone source terminology check passed all 1,965 files and the reverse patch check passed. Only comments and CLI help strings changed; no executable assertions, identifiers, diagnostics, behavior, dependency builds, or remote execution changed.

Copy the ordinary Rust executor and IxVM trace/CUDA outputs from the checked producer. Its grouped program matches the reviewed character-validation source, and both producer freshness checks pass. Sixteen producer outputs were copied and SHA256-verified; exactly five IxVM outputs change.